Step of Proof: gen_hyp_tp 9,38
Inference at * 1 1 4 2 1 1 
Iof proof for Lemma gen hyp tp:



1. A : Type
2. e : A
3. H : AType
4. x : A
5. e = x
6. z : H(x)
7. A  Type
8. e  A
9. x:A. (e = x)  Type
  z  0 
latex
 by %L:main% 
OnHyps [-1;-1;-1] Thin 
latex

On1: 

On1: 6. z : H(x)
On1:   z  0
On.

origin